\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $A$:ecl(${\it ds}$; ${\it da}$), ${\it upd}$:update{-}spec(${\it ds}$; ${\it da}$),\+
\\[0ex]${\it es}$:event\_system\{i:l\}, $z$:Id.
\-\\[0ex]($\uparrow$fpf{-}dom(id{-}deq; $z$; ${\it ds}$)) $\Rightarrow$ (ecl{-}mng{-}update\{i:l\}(${\it es}$; $i$; ${\it ds}$; ${\it da}$; $A$; $z$; ${\it upd}$) $\in$ prop\{i:l\})
\end{tabbing}